﻿// ==++==
// 
//   Copyright (c) Microsoft Corporation.  All rights reserved.
// 
// ==--==
using System;
using System.Collections.Generic;
using System.Text;
using Microsoft.ExtendedReflection.Reasoning.ExecutionNodes;
using Microsoft.Pex.Engine.SearchFrontiers;
using Microsoft.Pex.Engine.ComponentModel;
using Microsoft.ExtendedReflection.Collections;
using Microsoft.ExtendedReflection.Logging;
using Microsoft.ExtendedReflection.Utilities.Safe.Diagnostics;
using System.IO;
using Microsoft.ExtendedReflection.Utilities.Safe.Text;
using Microsoft.Pex.Engine.Logging;
using Microsoft.Pex.Fitness.Interfaces;

namespace Microsoft.Pex.Fitness.Implementation
{
    internal abstract class PexFitnessFrontierBase : IPexSearchFrontier
    {

        #region wrappers for frontiers
        class FitnessFrontierWrapper
        {
            private readonly SafeSortedDictionary<int, IPexSearchFrontier> frontiers = new SafeSortedDictionary<int, IPexSearchFrontier>();
            public IFiniteMap<int, IPexSearchFrontier> FitnessFrontier
            {
                get { return this.frontiers; }
            }

            private readonly SafeDictionary<IExecutionNode, int> nodes = new SafeDictionary<IExecutionNode, int>();
            public IFiniteSet<IExecutionNode> StoredNodes
            {
                get { return this.nodes.Keys; }
            }

            readonly PexLocatedInnerFrontierFactory<int> frontierFactory;
            public FitnessFrontierWrapper(PexLocatedInnerFrontierFactory<int> frontierFactory)
            {
                this.frontierFactory = frontierFactory;
            }

            public SafeSet<IExecutionNode> CloneNodes()
            {
                return new SafeSet<IExecutionNode>(this.nodes.Keys);
            }

            public void Add(IExecutionNode node, int fitness)
            {
                IPexSearchFrontier innerFrontier;
                if (!this.frontiers.TryGetValue(fitness, out innerFrontier))
                {
                    innerFrontier = this.frontierFactory(fitness);
                    this.frontiers[fitness] = innerFrontier;
                }
                SafeDebug.Assert((!innerFrontier.Contains(node)), "(!innerFrontier.Contains(node))");
                innerFrontier.Add(node);
                this.nodes.Add(node, fitness);
            }

            public bool TryGetNodeFitness(IExecutionNode node, out int fitness)
            {
                return this.nodes.TryGetValue(node, out fitness);
            }

            public void Remove(IExecutionNode node, bool used, IPexSearchFrontier innerFrontierExcluded)
            {
                int fitness;
                if (!this.nodes.TryGetValue(node, out fitness))
                {
                    SafeDebug.Fail("node is not contained");
                    return;
                }

                IPexSearchFrontier innerFrontier;
                if (this.frontiers.TryGetValue(fitness, out innerFrontier))
                {
                    if ((innerFrontierExcluded == null) || (innerFrontierExcluded != innerFrontier))
                    {
                        innerFrontier.Remove(node, used);
                        this.nodes.Remove(node);
                    }
                    if (!innerFrontier.HasContent)
                        this.frontiers.Remove(fitness);
                }
            }

            public bool TryRemove(out IExecutionNode node, out int fitness, out IPexSearchFrontier innerFrontierChosen)
            {
                foreach (var kvp in this.frontiers)
                {
                    fitness = kvp.Key;
                    innerFrontierChosen = kvp.Value;
                    if (innerFrontierChosen.TryRemove(out node))
                    {
                        this.nodes.Remove(node);//note that we need to do that here. for virtual id, the default frontier wrapper handles that 
                        return true;
                    }
                }

                node = null;
                fitness = 0;
                innerFrontierChosen = null;
                return false;
            }
        }
        #endregion

        private readonly Random random;
        const int VirtualTargetID = int.MaxValue;//this target id indicates that no target is encountered
        const int FitnessValueOfNodeForVirtualTarget = 1;//this value is not actually used, since the default frontier doesn't use this fitness value, we just give it a value in the fitness value place holder

        const int RewardPriorityAfterTargetFitnessImprovement = 1;//this value will be deducted (improved) from the priority value for a target whose fitness value has been improved during a run
        const int RewardPriorityMeritMultiplier = 2;//multiplier that kicks in when our strategy caused the fitness improvement
        const int PriorityLossAfterOneTimeUseOfTarget = 1;//this value will be added (degraded) from the priority value for a target when it is selected for corresponding node flipping.

        //the following threshold is set to give preference to real targets flipping which fitness improvement has been observed
        const int ThresholdForUnfruitfulFlipsForRealTargetsBeforeFlippingForVirttualTarget = 2;
        private int CounterForUnfruitfulFlipsForRealTargets = 0;
        private bool precedingFlipLeadToFitnessImprovement = false;
        private IExecutionNode ourLastFlippedNode;

        //the factory below is used to handle those nodes with the same fitness value w.r.t. a specific target
        private readonly PexLocatedInnerFrontierFactory<int> frontierFactory;

        private readonly IPexLog log;
        private readonly IPexFitnessExplorationManager fitnessExplorationManager;

        //Below is the design of the search frontier that can handle multiple targets (un-covered predicate 
        //side or branch involving binary integer comparison
        //
        /*   The frontiner is organized as below
         *    priority sorted ---->  target ID ----> <fitness sorted --> innerfrontier(nodes)>
         *    We use a wrapper class for <fitness sorted --> node> since we also use a node set to keep track
         *    which nodes have been stored in the innerfrontiers for the target
         */

        //for each target, initially its priority is 0
        //then each time it is picked, its priority is decreased by a constant PriorityLossAfterOneTimeUseOfTarget such as 1
        //but when the target's fitness value is improved for the previous picked run for it, 
        //its priority is increased by a constant RewardPriorityAfterTargetFitnessImprovement such as 5
        //To consider: Do we need to reset them every now and then? Currently not

        //when we encounter a node that is not related to any real target, we associate
        //it with a virtual target with target id as VirtualTargetID (a special value to avoid collision)
        //this virtual target's priority is 0 and would never be changed (if needed we can allow it to be changed but currently remain unchanged)
        //the fitness value of the node associated with this virtual target is FitnessValueOfNodeForVirtualTarget, e.g., 1 (never changed)

        //when a target is covered, we shall remove all the nodes for it and move the nodes to the above virtual
        //target's enry

        //we also have a mechnism to give priority to the frontiers of real targets if their fitness values
        //have been observed to have improvement over a certain number of runs/flips. 
        //In such cases, we don't give fair share to the default frontier (for the virtual target id).
        //See above ThresholdForUnfruitfulFlipsForRealTargetsBeforeFlippingForVirttualTarget for such uses

        //Overall, we use targetToFrontiers for dealing with frontiers for nodes w.r.t. normal targets
        //we use defaultFrontierWrapper for dealing with nodes w.r.t. the virtual target

        //indicates how many nodes have been removed, used only at dump statistics 
        private int removed;

        protected PexFitnessFrontierBase(
            IPexExplorationEngine host,
            Random random,
            PexLocatedInnerFrontierFactory<int> frontierFactory)//used to handle normal target ID
        {
            SafeDebug.AssumeNotNull(host, "host");
            SafeDebug.AssumeNotNull(random, "random");
            SafeDebug.AssumeNotNull(frontierFactory, "frontierFactory");

            this.log = (IPexLog)host.Log;
            this.random = random;
            this.frontierFactory = frontierFactory;

            this.fitnessExplorationManager = host.GetService<IPexFitnessExplorationManager>();

            //blow are the event handlers for allowing info from exploration monitor to propagate
            //info back to the frontier here
            this.fitnessExplorationManager.OnFitness += new RemoteEventHandler<PexFitnessEventArgs>(fm_OnFitness);
            this.fitnessExplorationManager.OnTargetCoverage += new RemoteEventHandler<PexFitnessEventArgs>(fm_OnTargetCoverage);
            this.fitnessExplorationManager.OnTargetFitnessImprovement += new RemoteEventHandler<PexFitnessEventArgs>(fm_OnTargetFitnessImprovement);
        }

        protected abstract void InternalAdd(IExecutionNode node);

        public void Add(IExecutionNode node)
        {
            if (this.fitnessExplorationManager.IsLoggingEnabled)
                this.log.LogMessage("fitness", "Add node {0}", node);
            this.InternalAdd(node);
            if (this.fitnessExplorationManager.IsLoggingEnabled)
                this.log.LogMessage("fitness", "after Add node {0}", node);
            this.toLogString();//debugging use
        }

        protected abstract void InternalRemove(IExecutionNode node, bool used);
        public void Remove(IExecutionNode node, bool used)
        {
            if (this.fitnessExplorationManager.IsLoggingEnabled)
                this.log.LogMessage("fitness", "Remove node {0}, {1}", node, used);
            this.InternalRemove(node, used);
        }

        protected abstract bool InternalTryRemove(out IExecutionNode node);

        public bool TryRemove(out IExecutionNode node)
        {
            if (this.fitnessExplorationManager.IsLoggingEnabled)
                this.log.LogMessage("fitness", "TryRemove node");
            return this.InternalTryRemove(out node);
        }

        protected abstract void InternalLocationUpdated(IExecutionNode node);
        public void LocationUpdated(IExecutionNode node)//we don't normally invoke this method inside this file
        {
            //this.log.LogMessage("fitness", "LocationUpdated node {0}", node);
            this.InternalLocationUpdated(node);
            this.Remove(node, false);
            this.Add(node);
        }

        protected abstract bool InternalContains(IExecutionNode node);
        public bool Contains(IExecutionNode node)
        {
            return this.InternalContains(node);
        }

        protected abstract int InternalSkipMany();
        public int SkipMany()
        {
            return this.InternalSkipMany();
        }

        protected abstract bool InternalHasContent { get; }
        public bool HasContent
        {
            get { return this.InternalHasContent; }
        }

        public bool IsProgressing
        {
            get { return false; }
        }

        #region priority list helper methods

        private int GetUserDefinedPriority(int target)
        {
            var methods = this.fitnessExplorationManager.GetMethodsOfTargetHash(target);
            foreach (var m in methods)
            {
                int p;
                if (this.fitnessExplorationManager.TryGetUserPriority(m, out p))
                    return p;
            }
            return 0;
        }
        #endregion

        #region event handling
        void fm_OnFitness(PexFitnessEventArgs e)
        {
            SafeDebug.AssumeNotNull(e, "e");

            IExecutionNode node = e.Node;

            //this.log.LogMessage("fitness", "fm_OnFitness node {0}", node);

            bool hasKey = this.InternalContains(node);
            if (hasKey)
            {
                if (this.fitnessExplorationManager.IsLoggingEnabled)
                    this.log.LogMessage("fitness", "fm_OnFitness node {0}", node);
                //this.log.LogMessage("fitness", "**** RESETTING FITNESS of node {0} ", node);                
                this.Remove(node, false);
                this.Add(node);
            }
        }

        protected abstract void OnTargetCoverage(int target);

        void fm_OnTargetCoverage(PexFitnessEventArgs e)
        {
            SafeDebug.AssumeNotNull(e, "e");

            int target = e.TargetID;
#if DEBUG
            if (this.fitnessExplorationManager.IsLoggingEnabled)
                this.log.LogMessage("fitness", "fm_OnTargetCoverage target {0}: {1}", target, this.fitnessExplorationManager.GetTargetIDString(target));
#endif

            //we should never cover a virtual target id
            SafeDebug.Assert((target != VirtualTargetID), "(target != VirtualTargetID)");
            this.OnTargetCoverage(target);
        }

        protected abstract void OnTargetFitnessImprovement(IExecutionNode flippedNode, int target);

        void fm_OnTargetFitnessImprovement(PexFitnessEventArgs e)
        {
            SafeDebug.AssumeNotNull(e, "e");

            int target = e.TargetID;
#if DEBUG
            if (this.fitnessExplorationManager.IsLoggingEnabled)
                this.log.LogMessage("fitness", "fm_OnTargetFitnessImprovement target {0}: {1}", target, this.fitnessExplorationManager.GetTargetIDString(target));
#endif
            this.OnTargetFitnessImprovement(e.FlippedNode, target);
        }
        #endregion


        #region debugging helper methods
        public void DumpStatistics(DumpTreeWriter writer, int depth)
        {
            object token = writer.StartNode(this.GetType().Name);
            using (TextWriter textWriter = writer.CreateTextWriter())
            {
                textWriter.WriteLine("{0} nodes removed", this.removed);
                writer.CloseTextWriter(textWriter);
            }
            writer.EndNode(token);
        }

#if false
        int logCount = 0;//used to avoid log filtering
#endif
        private void toLogString()
        {
#if false
            //debugging use
            if (this.fitnessExplorationManager.IsLoggingVerboseEnabled)
            {
                logCount++;
                this.log.LogMessage("fitness", "{0}Internal frontier state~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~", logCount);
                var sb = new SafeStringBuilder();

                foreach (var priorityTargetSets in this.priorityToTargets)
                {
                    int priority = priorityTargetSets.Key;
                    SafeSet<int> targetSet = priorityTargetSets.Value;
                    sb.Length = 0;
                    foreach (int target in targetSet)
                    {
                        sb.Append(target + ",");
                    }
                    this.log.LogMessage("fitness", "{2}priorityTargetSets (priority) {0} -> target ids: {1}", priority, sb.ToString(), logCount);
                }

                sb.Length = 0;
                foreach (var targetsToPriorityPair in this.targetsToPriorities)
                {
                    sb.Append(targetsToPriorityPair.Key + "->" + targetsToPriorityPair.Value + ",");
                }
                this.log.LogMessage("fitness", "{1}targetsToPriorities target->priority: {0}", sb.ToString(), logCount);

                //SafeIntDictionary<SafeSortedDictionary<int, ISearchFrontier>> targetToFrontiers
                sb.Length = 0;
                foreach (var targetToFrontierPair in this.targetToFrontiers)
                {
                    FitnessFrontierWrapper fitnessValueToInnerfrontiersWrapper = targetToFrontierPair.Value;
                    SafeSet<IExecutionNode> NodeSet = new SafeSet<IExecutionNode>();
                    foreach (var fitnessValueToInnerfrontierPair in fitnessValueToInnerfrontiersWrapper.FitnessFrontier)
                    {
                        ISearchFrontier innerFrontier = fitnessValueToInnerfrontierPair.Value;
                        foreach (var nodesTargetFitnessPair in this.nodesTargetFitness)
                        {
                            IExecutionNode node = nodesTargetFitnessPair.Key;
                            if (innerFrontier.Contains(node))
                            {
                                NodeSet.Add(node);
                                sb.Append(targetToFrontierPair.Key + "->" + fitnessValueToInnerfrontierPair.Key + ":" + "N" + ((IExecutionNode)node).UniqueIndex + "\n");
                            }
                        }
                    }
                    sb.Append("\nstored node list: ");
                    foreach (var node in fitnessValueToInnerfrontiersWrapper.StoredNodes)
                    {
                        sb.Append("N" + ((IExecutionNode)node).UniqueIndex + "\n");
                    }
                    SafeDebug.Assert((NodeSet.Count == fitnessValueToInnerfrontiersWrapper.StoredNodes.Count), "(NodeSet.Count == fitnessValueToInnerfrontiersWrapper.StoredNodes.Count)");
                }
                this.log.LogMessage("fitness", "{1}targetToFrontiers target->frontier fitness: N? :\n {0}", sb.ToString(), logCount);

                SafeSet<IExecutionNode> nodeSetForVirtualID = new SafeSet<IExecutionNode>();
                //ISearchFrontier defaultFrontier
                sb.Length = 0;
                foreach (var nodesTargetFitnessPair in this.nodesTargetFitness)
                {
                    IExecutionNode node = nodesTargetFitnessPair.Key;
                    if (defaultFrontierWrapper.Contains(node))
                    {
                        sb.Append("N" + ((IExecutionNode)node).UniqueIndex + "\n");
                        nodeSetForVirtualID.Add(node);
                    }
                }
                sb.Append("\n default stored node list: ");
                foreach (var node in this.defaultFrontierWrapper.Nodes)
                {
                    sb.Append("N" + ((IExecutionNode)node).UniqueIndex + "\n");
                }
                this.log.LogMessage("fitness", "{1}defaultFrontier :\n {0}", sb.ToString(), logCount);
                SafeDebug.Assert((nodeSetForVirtualID.Count == defaultFrontierWrapper.Nodes.Count), "(NodeSetForVirtualID.Count == defaultFrontierWrapper.StoredNodes.Count)");

                //SafeDictionary<IExecutionNode, SafeIntDictionary<int>> nodesTargetFitness
                sb.Length = 0;
                foreach (var nodesTargetFitnessPair in this.nodesTargetFitness)
                {
                    IExecutionNode node = nodesTargetFitnessPair.Key;
                    sb.Append("N" + ((IExecutionNode)node).UniqueIndex + ":\n");
                    SafeIntDictionary<int> targetFitness = nodesTargetFitnessPair.Value;
                    foreach (var targetFitnessPair in targetFitness)
                    {
                        sb.Append(targetFitnessPair.Key + "->" + targetFitnessPair.Value + ",");
                    }
                    sb.Append("\n");
                }
                this.log.LogMessage("fitness", "{1}nodesTargetFitness target->fitness value:\n {0}", sb.ToString(), logCount);

                if (this._coveredTargets != null)
                {
                    sb.Length = 0;
                    foreach (var target in this._coveredTargets)
                    {
                        sb.Append(target + ", ");
                        SafeDebug.Assert((!this.targetsToPriorities.ContainsKey(target)), "(!this.targetsToPriorities.ContainsKey(target))");
                        SafeDebug.Assert((!this.targetToFrontiers.ContainsKey(target)), "(!this.targetToFrontiers.ContainsKey(target))");
                    }
                    this.log.LogMessage("fitness", "CoveredTargets :\n {0}", sb.ToString());
                }
            }
#endif
        }
        #endregion

        public class OverallMinFitnessValueForAllTargets : PexFitnessFrontierBase
        {
            //OverallMinFitnessValueForAllTargets can be used when there is only one target to be considered globally
            //Currently it is used by selecting the min fitness values for all the targets. It is not a good option
            //But this generic frontier can be good for other situations when only one target is focused. So we keep it here
            //from fitness value -> inner frontiers
            private readonly SafeSortedDictionary<int, IPexSearchFrontier> fitnessIndexedInnerFrontiers = new SafeSortedDictionary<int, IPexSearchFrontier>();

            //from node -> fitness value (used to remember where to remove the node when it needs to removed)
            private readonly SafeDictionary<IExecutionNode, int> nodesFitness = new SafeDictionary<IExecutionNode, int>();

            public OverallMinFitnessValueForAllTargets(
                IPexExplorationEngine host,
                Random random,
                PexLocatedInnerFrontierFactory<int> frontierFactory,//used to handle normal target ID
                IPexSearchFrontier defaultFrontier) //used to handle VirtualTargetID
                : base(host, random, frontierFactory)
            {
            }

            protected override void InternalAdd(IExecutionNode node)
            {
                SafeDebug.AssertNotNull(this.fitnessIndexedInnerFrontiers, "fitnessIndexedInnerFrontiers");
                SafeDebug.AssertNotNull(this.nodesFitness, "nodesFitness");
                SafeDebug.Assert((!this.nodesFitness.ContainsKey(node)), "(!this.nodes.ContainsKey(node))");
                int fitness = this.fitnessExplorationManager.GetComputedFitness(node);
                //this.log.LogMessage("fitness", "**** ADDING node {0} with fitness value {1} ", node, fitness);
                this.nodesFitness.Add(node, fitness);
                IPexSearchFrontier innerFrontier;
                if (!this.fitnessIndexedInnerFrontiers.TryGetValue(fitness, out innerFrontier))
                {
                    innerFrontier = this.frontierFactory(fitness);
                    this.fitnessIndexedInnerFrontiers[fitness] = innerFrontier;
                }
                SafeDebug.Assert((!innerFrontier.Contains(node)), "(!level.Contains(node))");
                innerFrontier.Add(node);
            }

            protected override void InternalRemove(IExecutionNode node, bool used)
            {
                SafeDebug.AssertNotNull(this.nodesFitness, "nodesFitness");
                SafeDebug.AssertNotNull(this.fitnessIndexedInnerFrontiers, "fitnessIndexedInnerFrontiers");
                SafeDebug.Assert((this.nodesFitness.ContainsKey(node)), "(this.nodesFitness.ContainsKey(node))");
                int oldFitnessValue = this.nodesFitness[node];
                IPexSearchFrontier innerFrontier = this.fitnessIndexedInnerFrontiers[oldFitnessValue];
                innerFrontier.Remove(node, used);
                if (!innerFrontier.HasContent)
                    this.fitnessIndexedInnerFrontiers.Remove(oldFitnessValue);
                this.nodesFitness.Remove(node);

                //if (used)
                //clean up the node from the monitor but note that if later a path encounters this node
                //again, it will be added to the internal data structure in the fitnessExplorationMonitor again
                //    this.fitnessExplorationMonitor.removeNode((IExecutionNode)node);     
            }

            protected override bool InternalTryRemove(out IExecutionNode node)
            {
                SafeDebug.AssertNotNull(this.nodesFitness, "nodesFitness");
                SafeDebug.AssertNotNull(this.fitnessIndexedInnerFrontiers, "fitnessIndexedInnerFrontiers");
                foreach (var kvp in this.fitnessIndexedInnerFrontiers)
                {
                    int fitness = kvp.Key;
                    IPexSearchFrontier innerFrontier = kvp.Value;
                    if (innerFrontier.TryRemove(out node))
                    {
                        SafeDebug.Assert(this.nodesFitness.ContainsKey(node), "this.nodesFitness.ContainsKey(node)");
                        //this.log.LogMessage("fitness", "**** select fitness value {0} \n            node {1} ", fitness, node);

#if DEBUG
                        //we pass the info to fitness exploration monitor so that the graph can display it
                        //note that here we don't know the target id because we are using min value among all target id
                        this.fitnessExplorationManager.SetSelectedFrontierInfo(0, fitness, int.MaxValue);//the priority has no meaning for this option
#endif

                        //clean up the node from the monitor but note that if later a path encounters this node
                        //again, it will be added to the internal data structure in the fitnessExplorationMonitor again
                        //this.fitnessExplorationMonitor.removeNode((IExecutionNode)node);
                        this.removed++;

                        this.nodesFitness.Remove(node);
                        if (!innerFrontier.HasContent)
                            this.fitnessIndexedInnerFrontiers.Remove(fitness);
                        return true;
                    }
                    SafeDebug.Assert(innerFrontier.HasContent, "level.HasContent");
                }

                if (this.fitnessExplorationManager.IsLoggingEnabled)
                    this.log.LogMessage("fitness", "no node available");
                node = null;
                return false;
            }

            protected override void InternalLocationUpdated(IExecutionNode node)
            {
                SafeDebug.AssertNotNull(this.nodesFitness, "nodesFitness");
                SafeDebug.Assert((this.nodesFitness.ContainsKey(node)), "(this.nodesFitness.ContainsKey(node))");
            }

            protected override bool InternalContains(IExecutionNode node)
            {
                SafeDebug.AssertNotNull(this.nodesFitness, "nodesFitness");
                return this.nodesFitness.ContainsKey(node);
            }

            protected override bool InternalHasContent
            {
                get
                {
                    SafeDebug.AssertNotNull(this.nodesFitness, "nodesFitness");
                    return this.nodesFitness.Count > 0;
                }
            }

            protected override void OnTargetCoverage(int target)
            {
            }

            protected override void OnTargetFitnessImprovement(IExecutionNode flippedNode, int target)
            {
            }

            protected override int InternalSkipMany()
            {
                return 0;
            }
        }

        class DefaultFrontierWrapper
        {
            public readonly IPexSearchFrontier DefaultFrontier;
            private readonly SafeSet<IExecutionNode> nodes = new SafeSet<IExecutionNode>();
            public IFiniteSet<IExecutionNode> Nodes
            {
                get { return this.nodes; }
            }

            public DefaultFrontierWrapper(IPexSearchFrontier frontier)
            {
                SafeDebug.AssertNotNull(frontier, "frontier");
                this.DefaultFrontier = frontier;
            }

            public bool Contains(IExecutionNode node)
            {
                return this.DefaultFrontier.Contains(node);
            }

            public void Add(IExecutionNode node)
            {
                if (!this.DefaultFrontier.Contains(node))
                //we may face cases where node is included in the default frontier already since we move nodes to default frontier when their targets are covered
                {
                    this.DefaultFrontier.Add(node);
                    this.nodes.Add(node);
                }
            }

            public void Remove(IExecutionNode node, bool used, IPexSearchFrontier innerFrontierExcluded)
            {
                if ((innerFrontierExcluded == null) || (innerFrontierExcluded != DefaultFrontier))
                {
                    this.DefaultFrontier.Remove(node, used);
                    this.nodes.Remove(node);
                }
            }

            public bool TryRemove(out IExecutionNode node)
            {
                bool success = this.DefaultFrontier.TryRemove(out node);
                if (success)
                    this.nodes.Remove(node);
                return success;
            }


            public int SkipMany()
            {
                return this.DefaultFrontier.SkipMany();
            }
        }

        public class AlternateForTargets : PexFitnessFrontierBase
        {
            //from priority value -> target ID set
            //the lower priority value the better
            private readonly SafeSortedDictionary<int, SafeSet<int>> priorityToTargets = new SafeSortedDictionary<int, SafeSet<int>>();
            //from target ID to priority value (to trace back when removing a target)
            private readonly SafeIntDictionary<int> targetsToPriorities = new SafeIntDictionary<int>();

            //from target ID -> FitnessFrontierWrapper (including nodes/frontiers sorted by fitness values)
            private readonly SafeIntDictionary<FitnessFrontierWrapper> targetToFrontiers = new SafeIntDictionary<FitnessFrontierWrapper>();

            //from node -> (target id -> fitness value) (used to remember where to remove the node when it needs to removed)
            private readonly SafeDictionary<IExecutionNode, SafeIntDictionary<int>> nodesTargetFitness = new SafeDictionary<IExecutionNode, SafeIntDictionary<int>>();

            //used for VirtualTargetID using default frontier
            private readonly DefaultFrontierWrapper defaultFrontierWrapper;

            //a set of already covered targets, although Exploration Monitor also maintains such a set,
            //we maintain here as well, since when we query targetFitness info for a node being added,
            //Exploration Monitor returns the info includnig the fitness for already covered targets
            //We need this map to avoid keeping track of the fitness info for already covered targets in frontiers
            private SafeSet<int> _coveredTargets;

            public AlternateForTargets(
                IPexExplorationEngine host,
                Random random,
                PexLocatedInnerFrontierFactory<int> frontierFactory,//used to handle normal target ID
                IPexSearchFrontier defaultFrontier)//used to handle VirtualTargetID
                : base(host, random, frontierFactory)
            {
                if (defaultFrontier != null)
                    this.defaultFrontierWrapper = new DefaultFrontierWrapper(defaultFrontier);
            }

            #region priorities
            private void addTargetToPriorityList(int target)
            {
                int priority;
                SafeSet<int> targetIDSet;

                if (!this.targetsToPriorities.TryGetValue(target, out priority))
                {
                    priority = this.GetUserDefinedPriority(target);
                    this.targetsToPriorities.Add(target, priority);
                }
                if (!this.priorityToTargets.TryGetValue(priority, out targetIDSet))
                {
                    targetIDSet = new SafeSet<int>();
                    this.priorityToTargets.Add(priority, targetIDSet);
                }
                targetIDSet.Add(target);
            }

            private void removeTargetFromPriorityList(int target)
            {
                int priority;
                if (this.targetsToPriorities.TryGetValue(target, out priority))
                {
                    this.targetsToPriorities.Remove(target);
                    SafeSet<int> targetSet = this.priorityToTargets[priority];
                    targetSet.Remove(target);
                    if (targetSet.Count == 0)
                        this.priorityToTargets.Remove(priority);
                }
            }
            #endregion

            #region nodesTargetFitness helper methods
            private int getFitnessValue(IExecutionNode node, int targetID)
            {
                SafeDebug.Assert(this.nodesTargetFitness.ContainsKey(node), "this.nodesTargetFitness.ContainsKey(node)");
                SafeIntDictionary<int> targetFitnessPair = this.nodesTargetFitness[node];
                SafeDebug.Assert(targetFitnessPair.ContainsKey(targetID), "targetFitnessPair.ContainsKey(taregetID)");
                return targetFitnessPair[targetID];
            }

            private void removeNodeForTarget(IExecutionNode node, int targetID)
            {
                SafeDebug.Assert(this.nodesTargetFitness.ContainsKey(node), "this.nodesTargetFitness.ContainsKey(node)");
                SafeIntDictionary<int> targetFitnessPair = this.nodesTargetFitness[node];
                SafeDebug.Assert(targetFitnessPair.ContainsKey(targetID), "targetFitnessPair.ContainsKey(taregetID)");
                targetFitnessPair.Remove(targetID);
            }

            private void addNodeForTarget(IExecutionNode node, int target, int fitness)
            {
                if (this.fitnessExplorationManager.IsLoggingEnabled)
                    this.log.LogMessage("fitness", "**** ADDING node {0} with fitness value {1} for target {2}", node, fitness, target);

                if (target == VirtualTargetID)
                {
                    if (this.defaultFrontierWrapper != null)
                    {
                        SafeDebug.Assert((!defaultFrontierWrapper.Contains(node)), "(!defaultFrontier.Contains(node))");
                        this.defaultFrontierWrapper.Add(node);
                    }
                }
                else
                {
                    FitnessFrontierWrapper fitnessIndexedInnerFrontiersForAlternateWrapper;
                    if (!this.targetToFrontiers.TryGetValue(target, out fitnessIndexedInnerFrontiersForAlternateWrapper))
                    {
                        fitnessIndexedInnerFrontiersForAlternateWrapper = new FitnessFrontierWrapper(this.frontierFactory);
                        this.targetToFrontiers[target] = fitnessIndexedInnerFrontiersForAlternateWrapper;
                    }
                    fitnessIndexedInnerFrontiersForAlternateWrapper.Add(node, fitness);
                }
                addTargetToPriorityList(target);
            }

            private void addNodeForTargetFitnessValue(IExecutionNode node, int targetID, int fitnessValue)
            {
                SafeIntDictionary<int> targetFitness; ;
                if (!this.nodesTargetFitness.TryGetValue(node, out targetFitness))
                {
                    targetFitness = new SafeIntDictionary<int>();
                    nodesTargetFitness.Add(node, targetFitness);
                }
                if (targetFitness.ContainsKey(targetID))
                    targetFitness.Remove(targetID);
                targetFitness.Add(targetID, fitnessValue);
            }
            #endregion

            protected override void InternalAdd(IExecutionNode node)
            {
                SafeDebug.Assert((!this.nodesTargetFitness.ContainsKey(node)), "(!this.nodesTargetFitness.ContainsKey(node))");

                // getting the fitness value info for the node from the exploration monitor

                IFiniteMap<int, PexCompositeFitnessValue> targetFitness = this.fitnessExplorationManager.GetTargetFitnessInfo(node);
                // mapping of target id to fitness value

                SafeIntDictionary<int> targetFitnessPair = new SafeIntDictionary<int>();
                bool anyNotCovered = false;
                foreach (var kvp in targetFitness)
                {
                    var target = kvp.Key;
                    if (this._coveredTargets == null ||
                        !this._coveredTargets.Contains(target))
                    {
                        PexCompositeFitnessValue cfv = kvp.Value;
                        int fitness = cfv.FitnessValue;
                        if (this.fitnessExplorationManager.UseBranchFitnessGain)//by default we consider fitness gain for physical branch when calcuatling final fitness value
                            fitness -= cfv.BranchFitnessGain; // we subtract because the smaller the better...
                        this.addNodeForTarget(node, target, fitness);
                        targetFitnessPair.Add(target, fitness);
                        anyNotCovered = true;
                    }
                }
                if (!anyNotCovered)
                {
                    //when there is no target ID associated with the node, we associate it with virutal target id
                    //we give FitnessValueOfNodeForVirtualTarget fitness value for all ZeroTargetID
                    this.addNodeForTarget(node, VirtualTargetID, FitnessValueOfNodeForVirtualTarget);
                    targetFitnessPair.Add(VirtualTargetID, FitnessValueOfNodeForVirtualTarget);
                }
                this.nodesTargetFitness.Add(node, targetFitnessPair);//we need to finally add to nodesTargetFitness to keep track what nodes have been stored in our frontiers
            }

            protected override void InternalRemove(IExecutionNode node, bool used)
            {
                this.removeNodeExceptSpecifiedInnerFrontier(node, used, null);
                //if (used)
                //clean up the node from the monitor but note that if later a path encounters this node
                //again, it will be added to the internal data structure in the fitnessExplorationMonitor again
                //    this.fitnessExplorationMonitor.removeNode((IExecutionNode)node);     
            }

            private void updateTargetPriority(int targetID, int diff)
            {
                SafeDebug.Assert((this.targetsToPriorities.ContainsKey(targetID)), "(this.targetsToPriorities.ContainsKey(targetID))");
                // TODO: Nikolai, check this.
                if (diff == 0) return;
                int oldPriority = this.targetsToPriorities[targetID];
                int newPriority = oldPriority + diff;

                this.targetsToPriorities.Remove(targetID);
                this.targetsToPriorities.Add(targetID, newPriority);

                SafeSet<int> targetIDSet;
                if (this.priorityToTargets.TryGetValue(oldPriority, out targetIDSet))
                {
                    targetIDSet.Remove(targetID);
                    if (targetIDSet.Count == 0)
                        this.priorityToTargets.Remove(oldPriority);
                }
                SafeSet<int> targetIDSet2;
                if (!this.priorityToTargets.TryGetValue(newPriority, out targetIDSet2))
                {
                    targetIDSet2 = new SafeSet<int>();
                    priorityToTargets[newPriority] = targetIDSet2;
                }
                targetIDSet2.Add(targetID);
            }

            private void postHandlingAfterTryRemove(IExecutionNode node, IPexSearchFrontier usedFrontier, int fitness, int targetIDChosen, int priority)
            {
                SafeDebug.Assert(this.nodesTargetFitness.ContainsKey(node), "this.nodesTargetFitness.ContainsKey(node)");

                //we need to remove all other places (i.e., frontiers for other targets) that include this node
                //but no need to remove it from the current frontier (TryRemove handles that already)
                this.removeNodeExceptSpecifiedInnerFrontier(node, true, usedFrontier);

#if DEBUG
                if (this.fitnessExplorationManager.IsLoggingEnabled)
                    this.log.LogMessage("fitness", "**** select fitness value {0} \n            node {1} for target {2}:{4} with priority {3}", fitness, node, targetIDChosen, priority, this.fitnessExplorationManager.GetTargetIDString(targetIDChosen));

                //we pass the info to fitness exploration monitor so that the graph can display it
                this.fitnessExplorationManager.SetSelectedFrontierInfo(targetIDChosen, fitness, priority);
#endif
                //TODO: the following clean up is disabled since it may cause problems if we clean it up
                //need further debugging if we need better performance with lower memory overhead
                //=============
                //clean up the node from the monitor but note that if later a path encounters this node
                //again, it will be added to the internal data structure in the fitnessExplorationMonitor again
                //this.fitnessExplorationMonitor.removeNode((IExecutionNode)node);

                this.removed++;

                //we next reduce the priority of the target that the chosen node is for
                //we need to do this following check since if the removed node is the last node for 
                //a target, that target doesn't exist in the targetsToPriorities
                if (targetsToPriorities.ContainsKey(targetIDChosen))
                {
                    int oldPriority = targetsToPriorities[targetIDChosen];
                    this.updateTargetPriority(targetIDChosen, 1);//we give 1 point priority penalty
                }
                //this.toLogString();//debugging use
            }


            //this method is invoked when we need to remove all other places that include the given node being 
            //removed from a specific inner frontier. Then this method won't remove again the specific inner frontier
            //when innerFrontierExcluded is null, then we remove the node from all places.
            private void removeNodeExceptSpecifiedInnerFrontier(IExecutionNode node, bool used, IPexSearchFrontier innerFrontierExcluded)
            {
                SafeDebug.Assert((this.nodesTargetFitness.ContainsKey(node)), "(this.nodesTargetFitness.ContainsKey(node))");

                SafeIntDictionary<int> oldTargetFitness = this.nodesTargetFitness[node];
                foreach (var kvp in oldTargetFitness)
                {
                    int target = kvp.Key;
                    int oldFitnessValue = kvp.Value;

                    if (target == VirtualTargetID)
                    {
                        if (this.defaultFrontierWrapper != null)
                            this.defaultFrontierWrapper.Remove(node, used, innerFrontierExcluded);
                    }
                    else
                    {
                        FitnessFrontierWrapper fitnessIndexedInnerFrontiersForAlternateWrapper;
                        if (this.targetToFrontiers.TryGetValue(target, out fitnessIndexedInnerFrontiersForAlternateWrapper))
                        {
                            int otherOldFitnessValue;
                            if (fitnessIndexedInnerFrontiersForAlternateWrapper.TryGetNodeFitness(node, out otherOldFitnessValue))
                            {
                                SafeDebug.Assert(otherOldFitnessValue == oldFitnessValue, "otherOldFitnessValue == oldFitnessValue");
                                fitnessIndexedInnerFrontiersForAlternateWrapper.Remove(node, used, innerFrontierExcluded);
                            }
                        }
                    }
                }
                this.nodesTargetFitness.Remove(node);
            }

            protected override bool InternalTryRemove(out IExecutionNode node)
            {
                if (!precedingFlipLeadToFitnessImprovement)
                    CounterForUnfruitfulFlipsForRealTargets++;
                else
                    CounterForUnfruitfulFlipsForRealTargets = 0;
                precedingFlipLeadToFitnessImprovement = false;

                foreach (var priorityTargetSets in this.priorityToTargets)
                {
                    int priority = priorityTargetSets.Key;

                    SafeSet<int> targetSet = priorityTargetSets.Value;
                    SafeDebug.Assert(targetSet.Count > 0, "targetSet.Count > 0");
                    foreach (var targetIDChosen in targetSet.GetPermutation(this.random))
                    {
                        if (targetIDChosen == VirtualTargetID)
                        {
                            //if we haven't failed in improving any real target's fitness for the threshold time, we don't try virtual ID
                            if ((CounterForUnfruitfulFlipsForRealTargets < ThresholdForUnfruitfulFlipsForRealTargetsBeforeFlippingForVirttualTarget)
                                && (defaultFrontierWrapper == null || defaultFrontierWrapper.Nodes.Count < nodesTargetFitness.Count))
                                //note that it is possible that there are no nodes in the frontiers for real targets
                                //in such as case, if we skip our frontier for virtual ID, we will mistakenly 
                                //terminate the exploration saying no nodes to flip.
                                //to deal with such a case, we have the above second predicate to approximate 
                                //the determination of the case: we skip if the node number in the virtual id frontier 
                                //is less than the node number in all the frontiers.
                                continue;

                            if (this.defaultFrontierWrapper == null)
                                continue;

                            if (this.defaultFrontierWrapper.TryRemove(out node))
                            {
                                postHandlingAfterTryRemove(node, this.defaultFrontierWrapper.DefaultFrontier, FitnessValueOfNodeForVirtualTarget, targetIDChosen, priority);
                                if (this.fitnessExplorationManager.IsLoggingEnabled)
                                    this.log.LogMessage("fitness", "after TryRemove getting node {0} for virtual target id {1} (priority: {2}) with default fitness value {3}", node, targetIDChosen, priority, FitnessValueOfNodeForVirtualTarget);
                                this.toLogString();//debugging use
                                return true;
                            }
                        }
                        else
                        {
                            FitnessFrontierWrapper fitnessIndexedInnerFrontiersForAlternateWrapper;
                            if (this.targetToFrontiers.TryGetValue(targetIDChosen, out fitnessIndexedInnerFrontiersForAlternateWrapper))
                            {
                                int fitness;
                                IPexSearchFrontier innerFrontier;
                                if (fitnessIndexedInnerFrontiersForAlternateWrapper.TryRemove(out node, out fitness, out innerFrontier))
                                {
                                    this.ourLastFlippedNode = node;
                                    postHandlingAfterTryRemove(node, innerFrontier, fitness, targetIDChosen, priority);
                                    /*!!*/if (this.fitnessExplorationManager.IsLoggingEnabled)
                                        this.log.LogMessage("fitness", "after TryRemove getting node {0} at {1} for target id {2} (priority: {3}) with default fitness value {4}", node, node.CodeLocation.ToString(), targetIDChosen, priority, fitness);
                                    this.toLogString();//debugging use
                                    this.log.LogMessage("fitness", "choose {0}", node);
                                    return true;
                                }
                            }
                        }
                    }
                }

                if (this.fitnessExplorationManager.IsLoggingEnabled)
                    this.log.LogMessage("fitness", "no node available after TryRemove");
                node = null;
                this.toLogString();//debugging use
                return false;
            }

            protected override void InternalLocationUpdated(IExecutionNode node)
            {
                SafeDebug.Assert((this.nodesTargetFitness.ContainsKey(node)), "(this.nodesTargetFitness.ContainsKey(node))");
            }

            protected override bool InternalContains(IExecutionNode node)
            {
                return this.nodesTargetFitness.ContainsKey(node);
            }

            protected override bool InternalHasContent
            {
                get { return this.nodesTargetFitness.Count > 0; }
            }

            protected override void OnTargetCoverage(int target)
            {
                this.removeTargetFromPriorityList(target);

                FitnessFrontierWrapper fitnessIndexedInnerFrontiersForAlternateWrapper;
                if (this.targetToFrontiers.TryGetValue(target, out fitnessIndexedInnerFrontiersForAlternateWrapper))
                {
                    SafeSet<IExecutionNode> tempNodeSet = fitnessIndexedInnerFrontiersForAlternateWrapper.CloneNodes(); //used to avoid removing nodes when iterating through the nodes
                    foreach (var node in tempNodeSet)
                    {
                        if (!this.nodesTargetFitness.ContainsKey(node))
                            continue;
                        int fitnessValue = getFitnessValue(node, target);
                        int otherFitnessValue;
                        if (!fitnessIndexedInnerFrontiersForAlternateWrapper.TryGetNodeFitness(node, out otherFitnessValue))
                            SafeDebug.Fail("unreachable");
                        else
                            SafeDebug.Assert(otherFitnessValue == fitnessValue, "otherFitnessValue == fitnessValue");
                        //we remove this node from the current frontier (but not removing it from other places in other frontiers
                        fitnessIndexedInnerFrontiersForAlternateWrapper.Remove(node, false, null);
                        removeNodeForTarget(node, target);//for nodesTargetFitness 
                        //add it to the default frontier for the virtual target id
                        if (this.defaultFrontierWrapper != null)
                            this.defaultFrontierWrapper.Add(node);
                        addNodeForTargetFitnessValue(node, VirtualTargetID, 0);//for nodesTargetFitness
                    }
                }
                targetToFrontiers.Remove(target);
                if (this._coveredTargets == null)
                    this._coveredTargets = new SafeSet<int>();
                this._coveredTargets.Add(target);
                this.toLogString();
            }

            protected override void OnTargetFitnessImprovement(IExecutionNode flippedNode, int target)
            {
                /*!!*/if (this.fitnessExplorationManager.IsLoggingEnabled)
                this.log.LogMessage("fitness", "target fitness improved after flipping {0}", flippedNode);

                bool merit = false;
                //we record that this flipping cause at least some fitness improvement
                if (this.ourLastFlippedNode == flippedNode)
                {
                    precedingFlipLeadToFitnessImprovement = true;
                    /*!!*/if (this.fitnessExplorationManager.IsLoggingEnabled)
                        this.log.LogMessage("fitness", "our choice improved fitness");
                    this.log.LogMessage("fitness", "progress on {0} after flipping {1}", target, flippedNode);
                    merit = true;
                }
                else
                    this.log.LogMessage("fitness", "improvement on {0} after flipping {1}", target, flippedNode);

                //we promote the priority of the target by a specified reward constant
                if (this.targetsToPriorities.ContainsKey(target))
                {
                    updateTargetPriority(target, -RewardPriorityAfterTargetFitnessImprovement * (merit ? RewardPriorityMeritMultiplier : 1));

                    /*!!*/if (this.fitnessExplorationManager.IsLoggingEnabled)
                        this.log.LogMessage("fitness", "rewarded target {0} to {1}", target, this.targetsToPriorities[target]);
                }
                this.toLogString();
            }

            protected override int InternalSkipMany()
            {
                if (this.defaultFrontierWrapper == null)
                    return 0;
                else
                    return this.defaultFrontierWrapper.SkipMany();
            }
        }
    }
}
